0 Prolog
↳1 PrologToPiTRSProof (⇒, 62 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 57 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 10 ms)
↳25 QDP
↳26 MRRProof (⇔, 246 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 0 ms)
↳29 QDP
↳30 UsableRulesProof (⇔, 0 ms)
↳31 QDP
↳32 QReductionProof (⇔, 6 ms)
↳33 QDP
↳34 QDPSizeChangeProof (⇔, 0 ms)
↳35 YES
merge_in_gga(X, [], X) → merge_out_gga(X, [], X)
merge_in_gga([], X, X) → merge_out_gga([], X, X)
merge_in_gga(.(A, X), .(B, Y), .(A, Z)) → U1_gga(A, X, B, Y, Z, le_in_gg(A, B))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(A, X, B, Y, Z, le_out_gg(A, B)) → U2_gga(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
merge_in_gga(.(A, X), .(B, Y), .(B, Z)) → U3_gga(A, X, B, Y, Z, gt_in_gg(A, B))
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_gga(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U4_gga(A, X, B, Y, Z, merge_out_gga(.(A, X), Y, Z)) → merge_out_gga(.(A, X), .(B, Y), .(B, Z))
U2_gga(A, X, B, Y, Z, merge_out_gga(X, .(B, Y), Z)) → merge_out_gga(.(A, X), .(B, Y), .(A, Z))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
merge_in_gga(X, [], X) → merge_out_gga(X, [], X)
merge_in_gga([], X, X) → merge_out_gga([], X, X)
merge_in_gga(.(A, X), .(B, Y), .(A, Z)) → U1_gga(A, X, B, Y, Z, le_in_gg(A, B))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(A, X, B, Y, Z, le_out_gg(A, B)) → U2_gga(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
merge_in_gga(.(A, X), .(B, Y), .(B, Z)) → U3_gga(A, X, B, Y, Z, gt_in_gg(A, B))
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_gga(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U4_gga(A, X, B, Y, Z, merge_out_gga(.(A, X), Y, Z)) → merge_out_gga(.(A, X), .(B, Y), .(B, Z))
U2_gga(A, X, B, Y, Z, merge_out_gga(X, .(B, Y), Z)) → merge_out_gga(.(A, X), .(B, Y), .(A, Z))
MERGE_IN_GGA(.(A, X), .(B, Y), .(A, Z)) → U1_GGA(A, X, B, Y, Z, le_in_gg(A, B))
MERGE_IN_GGA(.(A, X), .(B, Y), .(A, Z)) → LE_IN_GG(A, B)
LE_IN_GG(s(X), s(Y)) → U6_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U1_GGA(A, X, B, Y, Z, le_out_gg(A, B)) → U2_GGA(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
U1_GGA(A, X, B, Y, Z, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y), Z)
MERGE_IN_GGA(.(A, X), .(B, Y), .(B, Z)) → U3_GGA(A, X, B, Y, Z, gt_in_gg(A, B))
MERGE_IN_GGA(.(A, X), .(B, Y), .(B, Z)) → GT_IN_GG(A, B)
GT_IN_GG(s(X), s(Y)) → U5_GG(X, Y, gt_in_gg(X, Y))
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
U3_GGA(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_GGA(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U3_GGA(A, X, B, Y, Z, gt_out_gg(A, B)) → MERGE_IN_GGA(.(A, X), Y, Z)
merge_in_gga(X, [], X) → merge_out_gga(X, [], X)
merge_in_gga([], X, X) → merge_out_gga([], X, X)
merge_in_gga(.(A, X), .(B, Y), .(A, Z)) → U1_gga(A, X, B, Y, Z, le_in_gg(A, B))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(A, X, B, Y, Z, le_out_gg(A, B)) → U2_gga(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
merge_in_gga(.(A, X), .(B, Y), .(B, Z)) → U3_gga(A, X, B, Y, Z, gt_in_gg(A, B))
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_gga(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U4_gga(A, X, B, Y, Z, merge_out_gga(.(A, X), Y, Z)) → merge_out_gga(.(A, X), .(B, Y), .(B, Z))
U2_gga(A, X, B, Y, Z, merge_out_gga(X, .(B, Y), Z)) → merge_out_gga(.(A, X), .(B, Y), .(A, Z))
MERGE_IN_GGA(.(A, X), .(B, Y), .(A, Z)) → U1_GGA(A, X, B, Y, Z, le_in_gg(A, B))
MERGE_IN_GGA(.(A, X), .(B, Y), .(A, Z)) → LE_IN_GG(A, B)
LE_IN_GG(s(X), s(Y)) → U6_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U1_GGA(A, X, B, Y, Z, le_out_gg(A, B)) → U2_GGA(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
U1_GGA(A, X, B, Y, Z, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y), Z)
MERGE_IN_GGA(.(A, X), .(B, Y), .(B, Z)) → U3_GGA(A, X, B, Y, Z, gt_in_gg(A, B))
MERGE_IN_GGA(.(A, X), .(B, Y), .(B, Z)) → GT_IN_GG(A, B)
GT_IN_GG(s(X), s(Y)) → U5_GG(X, Y, gt_in_gg(X, Y))
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
U3_GGA(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_GGA(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U3_GGA(A, X, B, Y, Z, gt_out_gg(A, B)) → MERGE_IN_GGA(.(A, X), Y, Z)
merge_in_gga(X, [], X) → merge_out_gga(X, [], X)
merge_in_gga([], X, X) → merge_out_gga([], X, X)
merge_in_gga(.(A, X), .(B, Y), .(A, Z)) → U1_gga(A, X, B, Y, Z, le_in_gg(A, B))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(A, X, B, Y, Z, le_out_gg(A, B)) → U2_gga(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
merge_in_gga(.(A, X), .(B, Y), .(B, Z)) → U3_gga(A, X, B, Y, Z, gt_in_gg(A, B))
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_gga(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U4_gga(A, X, B, Y, Z, merge_out_gga(.(A, X), Y, Z)) → merge_out_gga(.(A, X), .(B, Y), .(B, Z))
U2_gga(A, X, B, Y, Z, merge_out_gga(X, .(B, Y), Z)) → merge_out_gga(.(A, X), .(B, Y), .(A, Z))
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
merge_in_gga(X, [], X) → merge_out_gga(X, [], X)
merge_in_gga([], X, X) → merge_out_gga([], X, X)
merge_in_gga(.(A, X), .(B, Y), .(A, Z)) → U1_gga(A, X, B, Y, Z, le_in_gg(A, B))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(A, X, B, Y, Z, le_out_gg(A, B)) → U2_gga(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
merge_in_gga(.(A, X), .(B, Y), .(B, Z)) → U3_gga(A, X, B, Y, Z, gt_in_gg(A, B))
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_gga(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U4_gga(A, X, B, Y, Z, merge_out_gga(.(A, X), Y, Z)) → merge_out_gga(.(A, X), .(B, Y), .(B, Z))
U2_gga(A, X, B, Y, Z, merge_out_gga(X, .(B, Y), Z)) → merge_out_gga(.(A, X), .(B, Y), .(A, Z))
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
merge_in_gga(X, [], X) → merge_out_gga(X, [], X)
merge_in_gga([], X, X) → merge_out_gga([], X, X)
merge_in_gga(.(A, X), .(B, Y), .(A, Z)) → U1_gga(A, X, B, Y, Z, le_in_gg(A, B))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(A, X, B, Y, Z, le_out_gg(A, B)) → U2_gga(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
merge_in_gga(.(A, X), .(B, Y), .(B, Z)) → U3_gga(A, X, B, Y, Z, gt_in_gg(A, B))
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_gga(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U4_gga(A, X, B, Y, Z, merge_out_gga(.(A, X), Y, Z)) → merge_out_gga(.(A, X), .(B, Y), .(B, Z))
U2_gga(A, X, B, Y, Z, merge_out_gga(X, .(B, Y), Z)) → merge_out_gga(.(A, X), .(B, Y), .(A, Z))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
U1_GGA(A, X, B, Y, Z, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y), Z)
MERGE_IN_GGA(.(A, X), .(B, Y), .(A, Z)) → U1_GGA(A, X, B, Y, Z, le_in_gg(A, B))
MERGE_IN_GGA(.(A, X), .(B, Y), .(B, Z)) → U3_GGA(A, X, B, Y, Z, gt_in_gg(A, B))
U3_GGA(A, X, B, Y, Z, gt_out_gg(A, B)) → MERGE_IN_GGA(.(A, X), Y, Z)
merge_in_gga(X, [], X) → merge_out_gga(X, [], X)
merge_in_gga([], X, X) → merge_out_gga([], X, X)
merge_in_gga(.(A, X), .(B, Y), .(A, Z)) → U1_gga(A, X, B, Y, Z, le_in_gg(A, B))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(A, X, B, Y, Z, le_out_gg(A, B)) → U2_gga(A, X, B, Y, Z, merge_in_gga(X, .(B, Y), Z))
merge_in_gga(.(A, X), .(B, Y), .(B, Z)) → U3_gga(A, X, B, Y, Z, gt_in_gg(A, B))
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(A, X, B, Y, Z, gt_out_gg(A, B)) → U4_gga(A, X, B, Y, Z, merge_in_gga(.(A, X), Y, Z))
U4_gga(A, X, B, Y, Z, merge_out_gga(.(A, X), Y, Z)) → merge_out_gga(.(A, X), .(B, Y), .(B, Z))
U2_gga(A, X, B, Y, Z, merge_out_gga(X, .(B, Y), Z)) → merge_out_gga(.(A, X), .(B, Y), .(A, Z))
U1_GGA(A, X, B, Y, Z, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y), Z)
MERGE_IN_GGA(.(A, X), .(B, Y), .(A, Z)) → U1_GGA(A, X, B, Y, Z, le_in_gg(A, B))
MERGE_IN_GGA(.(A, X), .(B, Y), .(B, Z)) → U3_GGA(A, X, B, Y, Z, gt_in_gg(A, B))
U3_GGA(A, X, B, Y, Z, gt_out_gg(A, B)) → MERGE_IN_GGA(.(A, X), Y, Z)
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U1_GGA(A, X, B, Y, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y))
MERGE_IN_GGA(.(A, X), .(B, Y)) → U1_GGA(A, X, B, Y, le_in_gg(A, B))
MERGE_IN_GGA(.(A, X), .(B, Y)) → U3_GGA(A, X, B, Y, gt_in_gg(A, B))
U3_GGA(A, X, B, Y, gt_out_gg(A, B)) → MERGE_IN_GGA(.(A, X), Y)
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
le_in_gg(x0, x1)
gt_in_gg(x0, x1)
U6_gg(x0, x1, x2)
U5_gg(x0, x1, x2)
U3_GGA(A, X, B, Y, gt_out_gg(A, B)) → MERGE_IN_GGA(.(A, X), Y)
gt_in_gg(s(X), zero) → gt_out_gg(s(X), zero)
POL(.(x1, x2)) = 2·x1 + x2
POL(MERGE_IN_GGA(x1, x2)) = 2·x1 + 2·x2
POL(U1_GGA(x1, x2, x3, x4, x5)) = x1 + 2·x2 + 2·x3 + 2·x4 + 2·x5
POL(U3_GGA(x1, x2, x3, x4, x5)) = 2·x1 + 2·x2 + 2·x3 + 2·x4 + x5
POL(U5_gg(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U6_gg(x1, x2, x3)) = x1 + x2 + x3
POL(gt_in_gg(x1, x2)) = 2·x1 + 2·x2
POL(gt_out_gg(x1, x2)) = 1 + 2·x1 + x2
POL(le_in_gg(x1, x2)) = x1 + x2
POL(le_out_gg(x1, x2)) = x1 + x2
POL(s(x1)) = 2·x1
POL(zero) = 2
U1_GGA(A, X, B, Y, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y))
MERGE_IN_GGA(.(A, X), .(B, Y)) → U1_GGA(A, X, B, Y, le_in_gg(A, B))
MERGE_IN_GGA(.(A, X), .(B, Y)) → U3_GGA(A, X, B, Y, gt_in_gg(A, B))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
le_in_gg(x0, x1)
gt_in_gg(x0, x1)
U6_gg(x0, x1, x2)
U5_gg(x0, x1, x2)
MERGE_IN_GGA(.(A, X), .(B, Y)) → U1_GGA(A, X, B, Y, le_in_gg(A, B))
U1_GGA(A, X, B, Y, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
gt_in_gg(s(X), s(Y)) → U5_gg(X, Y, gt_in_gg(X, Y))
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U5_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
le_in_gg(x0, x1)
gt_in_gg(x0, x1)
U6_gg(x0, x1, x2)
U5_gg(x0, x1, x2)
MERGE_IN_GGA(.(A, X), .(B, Y)) → U1_GGA(A, X, B, Y, le_in_gg(A, B))
U1_GGA(A, X, B, Y, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
le_in_gg(x0, x1)
gt_in_gg(x0, x1)
U6_gg(x0, x1, x2)
U5_gg(x0, x1, x2)
gt_in_gg(x0, x1)
U5_gg(x0, x1, x2)
MERGE_IN_GGA(.(A, X), .(B, Y)) → U1_GGA(A, X, B, Y, le_in_gg(A, B))
U1_GGA(A, X, B, Y, le_out_gg(A, B)) → MERGE_IN_GGA(X, .(B, Y))
le_in_gg(s(X), s(Y)) → U6_gg(X, Y, le_in_gg(X, Y))
le_in_gg(zero, s(Y)) → le_out_gg(zero, s(Y))
le_in_gg(zero, zero) → le_out_gg(zero, zero)
U6_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
le_in_gg(x0, x1)
U6_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs: